-
Notifications
You must be signed in to change notification settings - Fork 106
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Trace Monad refactor #664
Trace Monad refactor #664
Conversation
aa3ec99
to
e3dde74
Compare
lib/Monads/trace/Trace_Monad.thy
Outdated
The following two instantiations are convenient to separate reasoning for exceptional and | ||
normal case.\<close> | ||
(* Narrator: they are in fact not convenient, and are now considered a mistake that should have | ||
been an abbreviation instead. *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
does this indicate this should be a FIXME?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe? This comment is copied verbatim from the nondet monad though, so I'd prefer not to change it as part of this work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
FIXME would indicate intent to change it. I think we probably don't want to change this, but we should also record that it probably wasn't the optimal decision to go with this in the first place.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To clarify, there actually is a FIXME on the definition in the following line, saying (* FIXME lib: this should be an abbreviation *)
See https://github.com/seL4/l4v/blob/master/lib/Monads/nondet/Nondet_VCG.thy#L66
@@ -645,7 +653,8 @@ subsection "Loops" | |||
text \<open> | |||
Loops are handled using the following inductive predicate; | |||
non-termination is represented using the failure flag of the | |||
monad.\<close> | |||
monad. | |||
FIXME: update comment about non-termination\<close> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
was this FIXME intended to be left in?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sort of, or at least it still needs to be updated. I'll either need to stare at this more to work out how non-termination is represented here or get help from someone who understands better how these loops are constructed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should leave the FIXME in. I don't think we have properly thought about how this should be defined yet. In particular, in the concurrent setting it does make sense to have a semantics for non-terminating loops, so the whole definition here might have to be rethought (or maybe a potentially non-terminating loop should get a separate definition).
apply (subst prefix_closed_def, clarsimp simp: bind_def) | ||
apply (auto simp: Cons_eq_append_conv split: tmres.split_asm | ||
dest!: prefix_closedD[rotated]; | ||
fastforce elim: rev_bexI) | ||
fastforce elim: rev_bexI) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this indent doesn't seem right
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The indent seems right to me, but the auto ...; fastforce
method is obviously terrible. I'll see if I can rework it into something nicer.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The fastforce
is to the left of the (
, which can't be right. The dest!:
on the auto
should align with the simp
, not the auto
, and then the fastforce
goes after the semicolon, so should be on the same level as the auto
.
NEVER MIND: this is an error between chair and keyboard, commit-by-commit reviews for large cleanups like this are difficult it seems.
That said, I agree with the method itself being terrible, but can deal with it another time.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also happy to leave this one for later, yes.
For commit messages, there are some that refer to |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a superb overhaul of the mess we had before, and you were way more thorough than I thought anyone would have the energy for. Many thanks and words of praise!
It's also a huge diff, so it was difficult to review. I didn't see anything moved to somewhere where it shouldn't have been. I had a few things I noticed or had questions about, but even if this goes in as-is it's a huge improvement. Further improvements should be incremental after this PR goes in, especially when we get to finally using the trace monad in more developments.
Good point, I'll try to make that consistent. |
ae6b076
to
08e13cb
Compare
The last force push did involve some new changes, but they were just restyling the theory imports to be consistent and hopefully aren't controversial. |
08e13cb
to
fada846
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work!
We might have this somewhere already and I missed it: do we have a lemma that shows that the Hoare triples are equivalent to RG-statements with R=G=UNIV? (Or is that not true?) If it is true, that's something we should probably add, which then leads to the question if triples should be an abbreviation. All of that is for another PR, looking through this material just made me think of the connection.
@@ -645,7 +653,8 @@ subsection "Loops" | |||
text \<open> | |||
Loops are handled using the following inductive predicate; | |||
non-termination is represented using the failure flag of the | |||
monad.\<close> | |||
monad. | |||
FIXME: update comment about non-termination\<close> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should leave the FIXME in. I don't think we have properly thought about how this should be defined yet. In particular, in the concurrent setting it does make sense to have a semantics for non-terminating loops, so the whole definition here might have to be rethought (or maybe a potentially non-terminating loop should get a separate definition).
apply (subst prefix_closed_def, clarsimp simp: bind_def) | ||
apply (auto simp: Cons_eq_append_conv split: tmres.split_asm | ||
dest!: prefix_closedD[rotated]; | ||
fastforce elim: rev_bexI) | ||
fastforce elim: rev_bexI) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also happy to leave this one for later, yes.
lib/Monads/trace/Trace_Monad.thy
Outdated
The following two instantiations are convenient to separate reasoning for exceptional and | ||
normal case.\<close> | ||
(* Narrator: they are in fact not convenient, and are now considered a mistake that should have | ||
been an abbreviation instead. *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
FIXME would indicate intent to change it. I think we probably don't want to change this, but we should also record that it probably wasn't the optimal decision to go with this in the first place.
Good idea, I don't think we have something like that yet. I'll see if it's easy to prove, and if it is then I'll add it in the next PR. |
fada846
to
32ec94e
Compare
32ec94e
to
b26156e
Compare
This should now be in sync with Nondet_Monad.thy wherever the two files have similar content. Signed-off-by: Corey Lewis <[email protected]>
This splits material out of Trace_Monad and Trace_VCG and into more specific theories, following the same approach and structure as the nondet theories. This commit is mainly focused on definitions and lemmas that also appear in the nondet monad; trace monad concepts are left where they are for now. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
b26156e
to
31b2a30
Compare
This PR refactors the Trace Monad to have the same general structure and style as the Nondet Monad. In particular:
valid
,validI
,no_fail
,no_trace
, etc.) and their lemmas are in their own files.The intentions for the commits in this PR and the reviewing suggestions are as follows: